InforLorV4, Main, Exploration, bibRecord, 007894

Reductions, intersection types, and explicit substitutions

Identifieur interne : 007894 ( Main/Exploration ); précédent : 007893; suivant : 007895

Reductions, intersection types, and explicit substitutions

Auteurs : Dan Dougherty [États-Unis] ; Pierre Lescanne [France]

Source :

Mathematical Structures in Computer Science [ 0960-1295 ] ; 2003-02.

RBID : ISTEX:27071424204977ABACF636C52BD08B3C1590E09A

Abstract

This paper is part of a general programme of treating explicit substitutions as the primary λ-calculi from the point of view of foundations as well as applications. We work in a composition-free calculus of explicit substitutions and an augmented calculus obtained by adding explicit garbage-collection, and explore the relationship between intersection-types and reduction. We show that the terms that normalise by leftmost reduction and the terms that normalise by head reduction can each be characterised as the terms typable in a certain system. The relationship between typability and strong normalisation is subtly different from the classical case: we show that typable terms are strongly normalising but give a counterexample to the converse. Our notions of leftmost and head reduction are non-deterministic, and our normalisation theorems apply to any computations obeying these strategies. In this way we refine and strengthen the classical normalisation theorems. The proofs require some new techniques in the presence of reductions involving explicit substitutions. Indeed, our proofs do not rely on results from classical λ-calculus, which in our view is subordinate to the calculus of explicit substitution.

Url:

https://api.istex.fr/ark:/67375/6GQ-WNF4V7G4-V/fulltext.pdf

DOI: 10.1017/S0960129502003821

Affiliations:

Links toward previous steps (curation, corpus...)

to stream Istex, to step Corpus: 000890
to stream Istex, to step Curation: 000885
to stream Istex, to step Checkpoint: 001883
to stream Main, to step Merge: 007C72
to stream Main, to step Curation: 007894

Le document en format XML

<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title>Reductions, intersection types, and explicit substitutions</title>
<author><name sortKey="Dougherty, Dan" sort="Dougherty, Dan" uniqKey="Dougherty D" first="Dan" last="Dougherty">Dan Dougherty</name>
</author>
<author><name sortKey="Lescanne, Pierre" sort="Lescanne, Pierre" uniqKey="Lescanne P" first="Pierre" last="Lescanne">Pierre Lescanne</name>
<affiliation><country>France</country>
<placeName><settlement type="city">Lyon</settlement>
<region type="region" nuts="2">Rhône-Alpes</region>
</placeName>
<orgName type="universitySchool" n="3">École normale supérieure de Lyon</orgName>
</affiliation>
</author>
</titleStmt>
<publicationStmt><idno type="wicri:source">ISTEX</idno>
<idno type="RBID">ISTEX:27071424204977ABACF636C52BD08B3C1590E09A</idno>
<date when="2003" year="2003">2003</date>
<idno type="doi">10.1017/S0960129502003821</idno>
<idno type="url">https://api.istex.fr/ark:/67375/6GQ-WNF4V7G4-V/fulltext.pdf</idno>
<idno type="wicri:Area/Istex/Corpus">000890</idno>
<idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">000890</idno>
<idno type="wicri:Area/Istex/Curation">000885</idno>
<idno type="wicri:Area/Istex/Checkpoint">001883</idno>
<idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Checkpoint">001883</idno>
<idno type="wicri:doubleKey">0960-1295:2003:Dougherty D:reductions:intersection:types</idno>
<idno type="wicri:Area/Main/Merge">007C72</idno>
<idno type="wicri:Area/Main/Curation">007894</idno>
<idno type="wicri:Area/Main/Exploration">007894</idno>
</publicationStmt>
<sourceDesc><biblStruct><analytic><title level="a">Reductions, intersection types, and explicit substitutions</title>
<author><name sortKey="Dougherty, Dan" sort="Dougherty, Dan" uniqKey="Dougherty D" first="Dan" last="Dougherty">Dan Dougherty</name>
<affiliation wicri:level="2"><country xml:lang="fr">États-Unis</country>
<placeName><region type="state">Connecticut</region>
</placeName>
<wicri:cityArea>Department of Mathematics and Computer Science, Wesleyan University, Middletown</wicri:cityArea>
</affiliation>
</author>
<author><name sortKey="Lescanne, Pierre" sort="Lescanne, Pierre" uniqKey="Lescanne P" first="Pierre" last="Lescanne">Pierre Lescanne</name>
<affiliation wicri:level="3"><country xml:lang="fr">France</country>
<wicri:regionArea>Laboratoire de l'Informatique du Parallélisme, École Normale Supérieure de Lyon, 46, Allée d'Italie, 69364 Lyon 07</wicri:regionArea>
<placeName><region type="region" nuts="2">Auvergne-Rhône-Alpes</region>
<region type="old region" nuts="2">Rhône-Alpes</region>
<settlement type="city">Lyon 07</settlement>
</placeName>
<placeName><settlement type="city">Lyon</settlement>
<region type="region" nuts="2">Rhône-Alpes</region>
</placeName>
<orgName type="universitySchool" n="3">École normale supérieure de Lyon</orgName>
</affiliation>
</author>
</analytic>
<monogr></monogr>
<series><title level="j">Mathematical Structures in Computer Science</title>
<idno type="ISSN">0960-1295</idno>
<idno type="eISSN">1469-8072</idno>
<imprint><publisher>Cambridge University Press</publisher>
<pubPlace>Cambridge, UK</pubPlace>
<date type="published" when="2003-02">2003-02</date>
<biblScope unit="volume">13</biblScope>
<biblScope unit="issue">1</biblScope>
<biblScope unit="page" from="55">55</biblScope>
<biblScope unit="page" to="85">85</biblScope>
</imprint>
<idno type="ISSN">0960-1295</idno>
</series>
</biblStruct>
</sourceDesc>
<seriesStmt><idno type="ISSN">0960-1295</idno>
</seriesStmt>
</fileDesc>
<profileDesc><textClass></textClass>
<langUsage><language ident="en">en</language>
</langUsage>
</profileDesc>
</teiHeader>
<front><div type="abstract">This paper is part of a general programme of treating explicit substitutions as the primary λ-calculi from the point of view of foundations as well as applications. We work in a composition-free calculus of explicit substitutions and an augmented calculus obtained by adding explicit garbage-collection, and explore the relationship between intersection-types and reduction. We show that the terms that normalise by leftmost reduction and the terms that normalise by head reduction can each be characterised as the terms typable in a certain system. The relationship between typability and strong normalisation is subtly different from the classical case: we show that typable terms are strongly normalising but give a counterexample to the converse. Our notions of leftmost and head reduction are non-deterministic, and our normalisation theorems apply to any computations obeying these strategies. In this way we refine and strengthen the classical normalisation theorems. The proofs require some new techniques in the presence of reductions involving explicit substitutions. Indeed, our proofs do not rely on results from classical λ-calculus, which in our view is subordinate to the calculus of explicit substitution.</div>
</front>
</TEI>
<affiliations><list><country><li>France</li>
<li>États-Unis</li>
</country>
<region><li>Auvergne-Rhône-Alpes</li>
<li>Connecticut</li>
<li>Rhône-Alpes</li>
</region>
<settlement><li>Lyon</li>
<li>Lyon 07</li>
</settlement>
<orgName><li>École normale supérieure de Lyon</li>
</orgName>
</list>
<tree><country name="États-Unis"><region name="Connecticut"><name sortKey="Dougherty, Dan" sort="Dougherty, Dan" uniqKey="Dougherty D" first="Dan" last="Dougherty">Dan Dougherty</name>
</region>
</country>
<country name="France"><region name="Auvergne-Rhône-Alpes"><name sortKey="Lescanne, Pierre" sort="Lescanne, Pierre" uniqKey="Lescanne P" first="Pierre" last="Lescanne">Pierre Lescanne</name>
</region>
</country>
</tree>
</affiliations>
</record>

Pour manipuler ce document sous Unix (Dilib)

EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Exploration

HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 007894 | SxmlIndent | more

HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 007894 | SxmlIndent | more

Pour mettre un lien sur cette page dans le réseau Wicri

{{Explor lien
   |wiki=    Wicri/Lorraine
   |area=    InforLorV4
   |flux=    Main
   |étape=   Exploration
   |type=    RBID
   |clé=     ISTEX:27071424204977ABACF636C52BD08B3C1590E09A
   |texte=   Reductions, intersection types, and explicit substitutions
}}

This area was generated with Dilib version V0.6.33.
Data generation: Mon Jun 10 21:56:28 2019. Site generation: Fri Feb 25 15:29:27 2022

	Serveur d'exploration sur la recherche en informatique en Lorraine
	Attention, ce site est en cours de développement ! Attention, site généré par des moyens informatiques à partir de corpus bruts. Les informations ne sont donc pas validées.

Serveur d'exploration sur la recherche en informatique en Lorraine

Reductions, intersection types, and explicit substitutions

Reductions, intersection types, and explicit substitutions

Source :

Abstract

Links toward previous steps (curation, corpus...)

Le document en format XML

Pour manipuler ce document sous Unix (Dilib)

Pour mettre un lien sur cette page dans le réseau Wicri